package org.korifey.ffbdd.impl;

import java.util.List;

import org.korifey.ffbdd.api.IBdd;
import org.korifey.ffbdd.api.IBddBackend;
import org.korifey.ffbdd.api.IBddDomain;
import org.korifey.ffbdd.api.INode;
import org.korifey.ffbdd.api.INonterminal;
import org.korifey.ffbdd.api.ITerminal;
import org.korifey.ffbdd.api.deprecated.Bdd;
import org.korifey.ffbdd.api.op.IBinaryOperation;
import org.korifey.ffbdd.api.op.IOpCache;
import org.korifey.ffbdd.api.op.OpCacheKey;
import org.korifey.ffbdd.api.op.OperationEnum;

import static org.korifey.ffbdd.api.util.NodeUtil.*;

public class BddDomainImpl implements IBddDomain {

	protected IBddBackend backend;
	protected IOpCache opCache;
	protected boolean lazy;
	protected int freeVar = 1000;
		
	public int acuireFreeVar() {
		return freeVar ++;
	}
	
	//Getters and setters
	public IBddBackend getBackend() {
		return backend;
	}

	public void setBackend(IBddBackend backend) {
		this.backend = backend;
	}

	public IOpCache getOpCache() {
		return opCache;
	}

	public void setOpCache(IOpCache opCache) {
		this.opCache = opCache;
	}
	
	
	private INode insertNonterminal(int var, INode one, INode zero) {
		return backend.insertNonterminal(var, one, zero);
	}
	
	private <E> ITerminal<E> insertTerminal(E value) {
		return backend.insertTerminal(value);
	}
	
	
	//Bdd constructors	
	public <T> ROBDD<T> makeConst(T value) {		
		return new ROBDD(insertTerminal(value), this);
	}
	
	public <T> ROBDD<T> makeNode(int var, T valueOne, T valueZero,
			boolean inversed) {		
		ITerminal<T> one = insertTerminal(valueOne);
		ITerminal<T> zero = insertTerminal(valueZero);
		INode n = (!inversed)?insertNonterminal(var, one, zero) : insertNonterminal(var, zero, one);
		return new ROBDD<T>(n, this);
	}
	

	
	@Override
	public boolean isLazy() {
		return lazy;
	}

	@Override
	public void setLazy(boolean lazy) {
		this.lazy = lazy;
	}

	//Binary operation
	public <T1, T2, T> ROBDD<T> applyBinary(IBdd<T1> b1, IBdd<T2> b2,
			IBinaryOperation<T1, T2, T> op) {
		
		return new ROBDD(_applyBinary(b1.getRoot(), b2.getRoot(), op), this);
	}
	
	private <T1, T2, T> INode _applyBinary(INode n1, INode n2, IBinaryOperation<T1, T2, T> op) {
		OpCacheKey key = new OpCacheKey.Binary(n1, n2, op.code()); 
		INode res = opCache.get(key);
		if (res != null) return res;
		
		if (n1.isTerm() && n2.isTerm()) {
			res = insertTerminal(op.apply(((ITerminal<T1>)n1).getValue(), ((ITerminal<T2>)n2).getValue()));
		} else {
			int var = _minVar(n1, n2);
			res = insertNonterminal(var,
					_applyBinary(_optOne(var, n1), _optOne(var, n2), op), 
					_applyBinary(_optZero(var, n1), _optZero(var, n2), op)
					);
		}
		opCache.put(key, res);
		return res;
	}
	
	@Override
	public <T> IBdd<T> ite(IBdd<Boolean> cond, IBdd<T> thenBranch,
			IBdd<T> elseBranch) {
		INode n = _applyBinary(cond.getRoot(), thenBranch.getRoot(), (IBinaryOperation)OperationEnum.IF.getOperation());
		INode res = _applyBinary(n, elseBranch.getRoot(), (IBinaryOperation)OperationEnum.NULL_REPLACE.getOperation());
		return new ROBDD(res, this);
	}

	@Override
	public List<IBdd<?>> listBDDs() {
		//TODO implement
		return null;
	}	
	

}
